package kb;

import java.io.IOException;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map.Entry;

import preprocessor.absorption.Absorption;
import preprocessor.absorption.BinaryAbsorption;
import preprocessor.absorption.ConceptAbsorption;
import preprocessor.absorption.EquivalenceAbsorption;
import preprocessor.absorption.RoleAbsorption;
import utils.exception.ConceptException;
import utils.io.KBAccess;
import entities.Axiom;
import entities.EquivalenceAxiom;
import entities.InclusionAxiom;
import entities.concept.AndConcept;
import entities.concept.Concept;
import entities.concept.NotConcept;
import entities.concept.PConcept;
import entities.vocabulary.Display;

/**
 * 
 * An unfoldable TBox Tu meets to the following conditions:
 * <br>1. of the form A=>C or A=C
 * <br>2. Axioms are unique, i.e.,A occurs only once on the LHS of all axioms
 * <br>3. Acyclic
 * <br>Note that it is necessary to perform absorption prior to this operation.
 * @see "DLHB"
 * @author j55wu
 *
 */
public class TBox {
	//axioms contains all the original axioms without any absorption ==> replaced by Tg alone
	//private HashMap<Concept,Concept> axioms = new HashMap<Concept,Concept>();
	//Tu contains axioms from absorption
	private HashMap<PConcept,Concept> Tu;
	//Tnu contains axioms from absorption on negated concept names
	private HashMap<NotConcept,Concept> Tnu;	
	//Tg contains GCIs.
	private HashMap<Concept,Concept> Tg;
	//Te contains eq axioms
	private HashMap<Concept,Concept> Te;
	//Tb only contains binary axioms from absorption.
	private HashMap<HashSet<PConcept>,Concept> Tb;
	private int numofAX;

	//get all the (f,v) during parsing
	//static public HashSet<DomainConcept> dcs = new HashSet<DomainConcept>();
	
	//private HashMap<Object, Object> domainMap;
	
	private boolean compiled;
	
	public void setNumAx(int na){
		this.numofAX = na;
	}
	
	public int getNumAx(){
		return this.numofAX;
	}
	
	public TBox deepcopyOfThisTBox(){
		TBox tb = new TBox();
		tb.compiled = this.compiled;
		tb.Tb.putAll(this.Tb);
		tb.Te.putAll(this.Te);
		tb.Tg.putAll(this.Tg);
		tb.Tnu.putAll(this.Tnu);
		tb.Tu.putAll(this.Tu);
		return tb;
	}
	public boolean getCompiledStatus(){
		return this.compiled;
	}
	
	public void setCompiledStatus(boolean b){
		this.compiled = b;
		return;
	}
	public TBox(){
		Tu = new HashMap<PConcept,Concept>();
		Tg = new HashMap<Concept,Concept>();
		Te = new HashMap<Concept,Concept>();
		//this mapping should contain all the parsed pairs of (= f k);
		//domainMap = new HashMap<Object, Object>();
		/*for(DomainConcept dc:dcs){
			this.insertDomainConcept(dc);
		}*/
		if(Absorption.BA){
			Tb = new HashMap<HashSet<PConcept>,Concept>();
		}
		if(Absorption.NCA){
			Tnu = new HashMap<NotConcept,Concept>();
		}
		this.compiled = false;
	}
	
	/**
	 * If absorptions generate any GCIs, save them somewhere for further absorptions.
	 * @see ConceptAbsorption
	 */
	public void saveGeneratedGCIs(Concept lhs, Concept rhs){
		insertTg(lhs,rhs);
	}
	
	public HashMap<PConcept,Concept> getTu(){
		return this.Tu;
	}
	
	public HashMap<NotConcept,Concept> getTnu(){
		return this.Tnu;
	}
	
	public HashMap<Concept,Concept> getTg(){
		return this.Tg;
	}
	
	public HashMap<Concept,Concept> getTe(){
		return this.Te;
	}
	
	public HashMap<HashSet<PConcept>,Concept> getTb(){
		return this.Tb;
	}
	
	public void mapAxiom(Axiom ax){
		//put an axiom in the map 
		if(ax instanceof InclusionAxiom){
			this.insertTg(ax);
		}else if(ax instanceof EquivalenceAxiom){
			this.insertTe((EquivalenceAxiom)ax);
		}
	}
	
	
	
	public HashMap<Concept,Concept> getInputAxioms(){
		return this.Tg;
	}

//
//	//check if the original TBox (i.e., original axioms) is unfoldable
//	private boolean isUnfoldable(){
//		//check condition 1
//		for(Concept c:this.Tg.keySet()){
//			if( ! (c instanceof PConcept) || c.isTop()){
//				insertTg(c, this.Tg.get(c));
//				this.Tg.remove(c);
//			}else{
//				//initial setup: put axioms into Tu.
//				try{
//					insertTu((PConcept)c, this.Tg.get(c));
//					this.Tg.remove(c);
//				}catch(Exception e){
//					e.printStackTrace();
//				}
//			}
//			assert this.Tg.isEmpty();
//		}
//		//check condition 2, automatically satisfied because we used HashMap: keys are unique.
//		//check condition 3
//		//not implemented yet, assume the TBox is designed to be acyclic.
//		
//		//if we have any GCI that needs to be considered by adding nondeterminism
//		if(Tg.size()>0){
//			return false;
//		}
//		return true;
//	}
	
	
	public void insertTe(EquivalenceAxiom ax){
		Concept lhs = ax.getLHS();
		if(Te.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Te.get(lhs));
			cons.add(ax.getRHS());
			Te.put(lhs, new AndConcept(cons));
		}else{
			Te.put(lhs, ax.getRHS());
		}
	}
	
	public void insertTe(Concept lhs, Concept rhs){
		if(Tg.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Te.get(lhs));
			cons.add(rhs);
			Te.put(lhs, new AndConcept(cons));
		}else{
			Te.put(lhs, rhs);
		}
	}
	
	
	/**
	 * A set of operations to push and get axioms for Tg, Tu, etc.
	 */
	public void insertTg(Axiom ax){
		Concept lhs = ax.getLHS();
		if(Tg.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tg.get(lhs));
			cons.add(ax.getRHS());
			Tg.put(lhs, new AndConcept(cons));
		}else{
			Tg.put(lhs, ax.getRHS());
		}
	}
	
	
	private void insertTg(Concept lhs, Concept rhs){
		if(Tg.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tg.get(lhs));
			cons.add(rhs);
			Tg.put(lhs, new AndConcept(cons));
		}else{
			Tg.put(lhs, rhs);
		}
	}
	
	public static void addToTBox(TBox tb, String fileName) throws IOException{
		HashSet<Axiom> axs = KBAccess.processAxiomFile(fileName);
		if(axs.size()>0){
			//add to Tg
			tb.insertTg(axs);
		}
		tb.setCompiledStatus(false);
		return;
	}
	
	//overloading
	public void insertTg(HashSet<Axiom> axs){
		for(Axiom ax: axs){
			insertTg(ax);
		}
	}
	
	public void insertTu(Axiom ax) throws ConceptException{
		if(! (ax.getLHS() instanceof PConcept)){
			throw new ConceptException("Axiom "+ax.toString()+" is not unfoldable.");
		}
		PConcept lhs = (PConcept) ax.getLHS();
		if(Tu.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tu.get(lhs));
			cons.add(ax.getRHS());
			Tu.put(lhs, new AndConcept(cons));
		}else{
			Tu.put(lhs, ax.getRHS());
		}
	}
	
	//overloading
	public void insertTu(PConcept lhs, Concept rhs) throws ConceptException{
//		if(! (lhs instanceof PConcept)){
//			throw new ConceptException("LHS "+Renderer.renderConcept(lhs)+" is not unfoldable.");
//		}
		PConcept plhs = (PConcept) lhs;
		if(Tu.keySet().contains(plhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tu.get(lhs));
			cons.add(rhs);
			Tu.put(plhs, new AndConcept(cons));
		}else{
			Tu.put(plhs, rhs);
		}
	}
	
	
	public void insertTu(HashSet<Axiom> axs){
		for(Axiom ax: axs){
			try{
				insertTu(ax);
			}catch(ConceptException e){
				e.printStackTrace();
			}
		}
	}
	
	
	public void insertTnu(Axiom ax) throws ConceptException{
		if(! (ax.getLHS() instanceof NotConcept)){
			throw new ConceptException("Axiom "+ax.toString()+" cannot be inserted into Tnu.");
		}
		NotConcept lhs = (NotConcept) ax.getLHS();
		if(Tnu.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tnu.get(lhs));
			cons.add(ax.getRHS());
			Tnu.put(lhs, new AndConcept(cons));
		}else{
			Tnu.put(lhs, ax.getRHS());
		}
	}
	
	//overoading
	public void insertTnu(NotConcept lhs, Concept rhs) throws ConceptException{
//		if(! (lhs instanceof NotConcept)){
//			throw new ConceptException("LHS mismatch! Axiom cannot be inserted into Tnu.");
//		}
		if(Tnu.keySet().contains(lhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tnu.get(lhs));
			cons.add(rhs);
			Tnu.put(lhs, new AndConcept(cons));
		}else{
			Tnu.put(lhs, rhs);
		}
	}
	
	public void insertTnu(HashSet<Axiom> axs){
		for(Axiom ax: axs){
			try{
				insertTnu(ax);
			}catch(ConceptException e){
				e.printStackTrace();
			}
		}
	}
	
	
	public void insertTb(Axiom ax) throws ConceptException{
		if(! (ax.getLHS() instanceof AndConcept)){
			//must be an AndConcept with two operands as PConcept
			throw new ConceptException("Axiom "+ax.toString()+" cannot be inserted into Tb.");
		}
		AndConcept lhs = (AndConcept)ax.getLHS();
		if(lhs.getConceptSet().size() != 2){
			throw new ConceptException("LHS Concept must contain only two named concepts!");
		}else{
			HashSet<PConcept> plhs = new HashSet<PConcept>();
			for(Concept c:lhs.getConceptSet()){
				 if(c instanceof PConcept){
					 plhs.add((PConcept)c);
				 }else{
					 throw new ConceptException("Concept "+c+" is not primitive. Cannot be iserted into Tb.");
				 }
			}
			if(Tb.keySet().containsAll(lhs.getConceptSet())){
				//already exists
				HashSet<Concept> cons = new HashSet<Concept>();
				cons.add(Tb.get(plhs));
				cons.add(ax.getRHS());
				Tb.put(plhs, new AndConcept(cons));
			}else{
				//new axiom into Tb
				Tb.put(plhs, ax.getRHS());
			}
			
		}
		return;
	}
	
	//Overloading this method to allow flexible binary absorption.
	public void insertTb(HashSet<Concept> lhs, Concept rhs) throws ConceptException{
		if(lhs.size() != 2){
			throw new ConceptException("LHS must contain only 2 concept names. Cannot be inserted into Tb.");
		}
		HashSet<PConcept> newlhs = new HashSet<PConcept>();
		for(Concept c:lhs){
			if(! (c instanceof PConcept)){
				throw new ConceptException("LHS not concept names for Tb.");
			}else{
				newlhs.add((PConcept)c);
			}
		}
		if(Tb.keySet().contains(newlhs)){
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tb.get(newlhs));
			cons.add(rhs);
			Tb.put(newlhs, new AndConcept(cons));
		}else{
			Tb.put(newlhs, rhs);
		}
		return;
	}
	
	public void insertTb(HashSet<Axiom> axs){
		for(Axiom ax: axs){
			try{
				insertTb(ax);
			}catch(ConceptException e){
				e.printStackTrace();
			}
		}
	}
	
	
	public boolean compileTBox(){
		if(! this.compiled){
			return absorbAxioms();
		}
		return true;
	}
	
	//fetch Tg axioms, and absorb
	private boolean absorbAxioms(){
		//String[] abs = Start.CONF.getProperty("absorptions").split(" ");
		boolean suc=false;
		//break equivalences
		if(Absorption.EQA || this.Te.size() > 0){
			EquivalenceAbsorption ea = new EquivalenceAbsorption(this);
			ea.absorb();
		}
		if(this.Tg.size()<1){
			suc = true;
			return suc;
		}
		if(Absorption.CA || Absorption.NCA || Absorption.ECA){
			ConceptAbsorption ca = new ConceptAbsorption(this);
			suc &= ca.absorb();
		}
		if(Absorption.BA){
			BinaryAbsorption ba = new BinaryAbsorption(this);
			suc &= ba.absorb();
		}
		if(Absorption.RA){
			RoleAbsorption ra = new RoleAbsorption(this);
			suc &= ra.absorb();
		}
		this.compiled = true;
		return suc;
	}
	

	/*public boolean testDomainConcept(Object f, Object k){
		if(this.domainMap.containsKey(f)){
			if(!k.equals(this.domainMap.get(f))){
				return false;
			}
		}
		return true;
	}*/
	

/*	public boolean insertDomainConcept(Object f, Object k){
		boolean insert=true;
		if(f instanceof Role && k instanceof Role){
			//replacement of forks???
		}else{
			Role r = (f instanceof Role)? (Role) f: (Role) k;
			Object v = (f instanceof Role)? k: f;
			if(!this.domainMap.containsKey(r)){
				//no such entry
				this.domainMap.put(r, v);
			}else if(!this.testDomainConcept(r, v)){
				//a clash!
				insert = false;
			}
		}
		return insert;
	}*/
	

/*	public boolean insertDomainConcept(DomainConcept dc){
		return this.insertDomainConcept(dc.getFeature(), dc.getValue());
	}*/
	
	/*public HashMap<Object, Object> getDomainMap(){
		return this.domainMap;
	}*/

	@Override
	public String toString(){
		String ret = "";
		ret += "\n=============\nAxioms in the TBox "+Display.TBOXUNICODE +":\n=============\n";
		HashMap<?, ?> maps[] = {Tu, Tnu, Tg, Te, Tb};
		for (HashMap<?, ?> map : maps) {
			for(Entry<?,?> e:map.entrySet()){
				ret += e.getKey().toString() + " => " + e.getValue()+"\n";
			}
		}
		return ret;
	}
	
	
}
